package com.googlecode.kipler.satisfiability.completion.rule.formula;

import com.googlecode.kipler.container.dl.FormulaCategory;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.completion.rule.CompletionRule;
import com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation.AndAlphaFormula;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;


/**
 * This rule finds all the conjunctions in the current world and adds both
 * operands of a conjunction to the current world.
 * 
 * @author İnanç Seylan
 * 
 */
public class AndRule extends CompletionRule {
	private AlphaFormulaRule alphaRule;

	public AndRule() {
		alphaRule = new AlphaFormulaRule(FormulaCategory.AND,
				new AndAlphaFormula(), "And rule");
	}

	public void apply() throws UnsatisfiableException {
		alphaRule.apply();
	}

	public WorldConstraintSystem getWcs() {
		return alphaRule.getWcs();
	}

	public World getWorld() {
		return alphaRule.getWorld();
	}

	public boolean isApplied() {
		return alphaRule.isApplied();
	}

	public void setWcs(WorldConstraintSystem wcs) {
		alphaRule.setWcs(wcs);
	}

	public void setWorld(World world) {
		alphaRule.setWorld(world);
	}

}
